g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldf(x, nil) → x
foldf(x, cons(y, z)) → f(foldf(x, z), y)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, cons(C, c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) → foldf(triple(a, b, nil), c)
↳ QTRS
↳ DependencyPairsProof
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldf(x, nil) → x
foldf(x, cons(y, z)) → f(foldf(x, z), y)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, cons(C, c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) → foldf(triple(a, b, nil), c)
FOLDF(x, cons(y, z)) → FOLDF(x, z)
F'(triple(a, b, c), A) → F''(foldf(triple(cons(A, a), nil, c), b))
F(t, x) → G(x)
FOLDF(x, cons(y, z)) → F(foldf(x, z), y)
F'(triple(a, b, c), B) → F(triple(a, b, c), A)
F(t, x) → F'(t, g(x))
F''(triple(a, b, c)) → FOLDF(triple(a, b, nil), c)
F'(triple(a, b, c), A) → FOLDF(triple(cons(A, a), nil, c), b)
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldf(x, nil) → x
foldf(x, cons(y, z)) → f(foldf(x, z), y)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, cons(C, c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) → foldf(triple(a, b, nil), c)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
FOLDF(x, cons(y, z)) → FOLDF(x, z)
F'(triple(a, b, c), A) → F''(foldf(triple(cons(A, a), nil, c), b))
F(t, x) → G(x)
FOLDF(x, cons(y, z)) → F(foldf(x, z), y)
F'(triple(a, b, c), B) → F(triple(a, b, c), A)
F(t, x) → F'(t, g(x))
F''(triple(a, b, c)) → FOLDF(triple(a, b, nil), c)
F'(triple(a, b, c), A) → FOLDF(triple(cons(A, a), nil, c), b)
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldf(x, nil) → x
foldf(x, cons(y, z)) → f(foldf(x, z), y)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, cons(C, c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) → foldf(triple(a, b, nil), c)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
FOLDF(x, cons(y, z)) → FOLDF(x, z)
F'(triple(a, b, c), A) → F''(foldf(triple(cons(A, a), nil, c), b))
FOLDF(x, cons(y, z)) → F(foldf(x, z), y)
F'(triple(a, b, c), B) → F(triple(a, b, c), A)
F(t, x) → F'(t, g(x))
F''(triple(a, b, c)) → FOLDF(triple(a, b, nil), c)
F'(triple(a, b, c), A) → FOLDF(triple(cons(A, a), nil, c), b)
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldf(x, nil) → x
foldf(x, cons(y, z)) → f(foldf(x, z), y)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, cons(C, c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) → foldf(triple(a, b, nil), c)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
FOLDF(x, cons(y, z)) → FOLDF(x, z)
F'(triple(a, b, c), A) → F''(foldf(triple(cons(A, a), nil, c), b))
FOLDF(x, cons(y, z)) → F(foldf(x, z), y)
F''(triple(a, b, c)) → FOLDF(triple(a, b, nil), c)
F'(triple(a, b, c), A) → FOLDF(triple(cons(A, a), nil, c), b)
Used ordering: Polynomial interpretation [25,35]:
F'(triple(a, b, c), B) → F(triple(a, b, c), A)
F(t, x) → F'(t, g(x))
The value of delta used in the strict ordering is 7/32.
POL(F''(x1)) = 1 + (2)x_1
POL(f''(x1)) = 1/4 + x_1
POL(g(x1)) = 0
POL(f(x1, x2)) = 1 + x_1
POL(C) = 0
POL(FOLDF(x1, x2)) = 1/2 + (2)x_1 + x_2
POL(A) = 1/4
POL(triple(x1, x2, x3)) = (1/4)x_1 + (4)x_2 + (1/2)x_3
POL(cons(x1, x2)) = 2 + (1/4)x_1 + x_2
POL(f'(x1, x2)) = 1 + x_1
POL(F'(x1, x2)) = 9/4 + (2)x_1
POL(B) = 0
POL(foldf(x1, x2)) = x_1 + (1/2)x_2
POL(F(x1, x2)) = 9/4 + (2)x_1
POL(nil) = 0
foldf(x, nil) → x
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f''(triple(a, b, c)) → foldf(triple(a, b, nil), c)
foldf(x, cons(y, z)) → f(foldf(x, z), y)
f'(triple(a, b, c), A) → f''(foldf(triple(cons(A, a), nil, c), b))
f'(triple(a, b, c), C) → triple(a, b, cons(C, c))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
F(t, x) → F'(t, g(x))
F'(triple(a, b, c), B) → F(triple(a, b, c), A)
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldf(x, nil) → x
foldf(x, cons(y, z)) → f(foldf(x, z), y)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, cons(C, c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) → foldf(triple(a, b, nil), c)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F'(triple(a, b, c), B) → F(triple(a, b, c), A)
Used ordering: Polynomial interpretation [25,35]:
F(t, x) → F'(t, g(x))
The value of delta used in the strict ordering is 1/8.
POL(F'(x1, x2)) = (1/4)x_2
POL(g(x1)) = (2)x_1
POL(B) = 1/2
POL(C) = 1/2
POL(A) = 0
POL(F(x1, x2)) = (4)x_2
POL(triple(x1, x2, x3)) = 5/2 + x_1 + (4)x_2
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
F(t, x) → F'(t, g(x))
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldf(x, nil) → x
foldf(x, cons(y, z)) → f(foldf(x, z), y)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, cons(C, c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) → foldf(triple(a, b, nil), c)